Nuprl Definition : ma-kind
0,22
postcript
pdf
Kind(
da
) == {
k
:Knd|
k
dom(
da
) }
latex
clarification:
Kind(
da
) == {
k
:Knd| fpf-dom(KindDeq;
k
;
da
) }
latex
Definitions
{
x
:
A
|
B
(
x
) }
,
Knd
,
b
,
x
dom(
f
)
,
KindDeq
FDL editor aliases
ma-kind
origin
dom(da) }
dom(da) }
b dom(f)